Inference at * 1 
Iof proof for Lemma hd-before:



1. T : Type
2. u : T
3. v : T List
4. 0 < (||v||+1)
5. x : T
6. (x  [u / v])
7. (x = u)
  u before x  [u / v] 

latex

 by ((((((RWO "cons_member" (-2)) 
THENM (D (-2)))) 
TCollapseTHEN (Auto))) 
TCollapseTHEN (((
TC((RWO "cons_before" 0) 
THENM (OrLeft))) 
TCollapseTHEN (Auto)))) 

latex

TC.

Definitions	left + right, False, n+m, ||as||, P  Q, P  Q, P  Q, P  Q, P & Q, x:A  B(x), A, (x  l), a < b, type List, Type, x before y  l, x:A. B(x), x:AB(x), t  T, s = t
Lemmas	cons member, cons before, l before wf